0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 2 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxWeightedTrs
↳7 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedTrs
↳9 CompletionProof (UPPER BOUND(ID), 0 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 8 ms)
↳12 CpxRNTS
↳13 CompleteCoflocoProof (⇔, 607 ms)
↳14 BOUNDS(1, n^2)
U11(tt, V2) → U12(isNat(activate(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, V2) → U32(isNat(activate(V2)))
U32(tt) → tt
U41(tt, N) → activate(N)
U51(tt, M, N) → U52(isNat(activate(N)), activate(M), activate(N))
U52(tt, M, N) → s(plus(activate(N), activate(M)))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(activate(N)), activate(M), activate(N))
U72(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(isNat(activate(V1)), activate(V2))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNat(n__x(V1, V2)) → U31(isNat(activate(V1)), activate(V2))
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)
x(X1, X2) → n__x(X1, X2)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__s(X)) → s(activate(X))
activate(n__x(X1, X2)) → x(activate(X1), activate(X2))
activate(X) → X
U11(tt, V2) → U12(isNat(activate(V2))) [1]
U12(tt) → tt [1]
U21(tt) → tt [1]
U31(tt, V2) → U32(isNat(activate(V2))) [1]
U32(tt) → tt [1]
U41(tt, N) → activate(N) [1]
U51(tt, M, N) → U52(isNat(activate(N)), activate(M), activate(N)) [1]
U52(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U61(tt) → 0 [1]
U71(tt, M, N) → U72(isNat(activate(N)), activate(M), activate(N)) [1]
U72(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNat(activate(V1)), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNat(activate(V1))) [1]
isNat(n__x(V1, V2)) → U31(isNat(activate(V1)), activate(V2)) [1]
plus(N, 0) → U41(isNat(N), N) [1]
plus(N, s(M)) → U51(isNat(M), M, N) [1]
x(N, 0) → U61(isNat(N)) [1]
x(N, s(M)) → U71(isNat(M), M, N) [1]
0 → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0 [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__x(X1, X2)) → x(activate(X1), activate(X2)) [1]
activate(X) → X [1]
| 0 => 0' |
U11(tt, V2) → U12(isNat(activate(V2))) [1]
U12(tt) → tt [1]
U21(tt) → tt [1]
U31(tt, V2) → U32(isNat(activate(V2))) [1]
U32(tt) → tt [1]
U41(tt, N) → activate(N) [1]
U51(tt, M, N) → U52(isNat(activate(N)), activate(M), activate(N)) [1]
U52(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U61(tt) → 0' [1]
U71(tt, M, N) → U72(isNat(activate(N)), activate(M), activate(N)) [1]
U72(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNat(activate(V1)), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNat(activate(V1))) [1]
isNat(n__x(V1, V2)) → U31(isNat(activate(V1)), activate(V2)) [1]
plus(N, 0') → U41(isNat(N), N) [1]
plus(N, s(M)) → U51(isNat(M), M, N) [1]
x(N, 0') → U61(isNat(N)) [1]
x(N, s(M)) → U71(isNat(M), M, N) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__x(X1, X2)) → x(activate(X1), activate(X2)) [1]
activate(X) → X [1]
plus(N, 0') → U41(isNat(N), N) [1]
plus(N, s(M)) → U51(isNat(M), M, N) [1]
x(N, 0') → U61(isNat(N)) [1]
x(N, s(M)) → U71(isNat(M), M, N) [1]
0' → n__0 [1]
s(X) → n__s(X) [1]
U11(tt, V2) → U12(isNat(activate(V2))) [1]
U12(tt) → tt [1]
U21(tt) → tt [1]
U31(tt, V2) → U32(isNat(activate(V2))) [1]
U32(tt) → tt [1]
U41(tt, N) → activate(N) [1]
U51(tt, M, N) → U52(isNat(activate(N)), activate(M), activate(N)) [1]
U52(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U61(tt) → 0' [1]
U71(tt, M, N) → U72(isNat(activate(N)), activate(M), activate(N)) [1]
U72(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNat(activate(V1)), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNat(activate(V1))) [1]
isNat(n__x(V1, V2)) → U31(isNat(activate(V1)), activate(V2)) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__x(X1, X2)) → x(activate(X1), activate(X2)) [1]
activate(X) → X [1]
U11(tt, V2) → U12(isNat(activate(V2))) [1]
U12(tt) → tt [1]
U21(tt) → tt [1]
U31(tt, V2) → U32(isNat(activate(V2))) [1]
U32(tt) → tt [1]
U41(tt, N) → activate(N) [1]
U51(tt, M, N) → U52(isNat(activate(N)), activate(M), activate(N)) [1]
U52(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U61(tt) → 0' [1]
U71(tt, M, N) → U72(isNat(activate(N)), activate(M), activate(N)) [1]
U72(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNat(activate(V1)), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNat(activate(V1))) [1]
isNat(n__x(V1, V2)) → U31(isNat(activate(V1)), activate(V2)) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__x(X1, X2)) → x(activate(X1), activate(X2)) [1]
activate(X) → X [1]
| U11 :: tt → n__0:n__plus:n__s:n__x → tt tt :: tt U12 :: tt → tt isNat :: n__0:n__plus:n__s:n__x → tt activate :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U21 :: tt → tt U31 :: tt → n__0:n__plus:n__s:n__x → tt U32 :: tt → tt U41 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U51 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U52 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x s :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x plus :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U61 :: tt → n__0:n__plus:n__s:n__x 0' :: n__0:n__plus:n__s:n__x U71 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U72 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x x :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x n__0 :: n__0:n__plus:n__s:n__x n__plus :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x n__s :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x n__x :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x |
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
tt => 0
n__0 => 0
0' -{ 1 }→ 0 :|:
U11(z, z') -{ 1 }→ U12(isNat(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U12(z) -{ 1 }→ 0 :|: z = 0
U21(z) -{ 1 }→ 0 :|: z = 0
U31(z, z') -{ 1 }→ U32(isNat(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U32(z) -{ 1 }→ 0 :|: z = 0
U41(z, z') -{ 1 }→ activate(N) :|: z' = N, z = 0, N >= 0
U51(z, z', z'') -{ 1 }→ U52(isNat(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U52(z, z', z'') -{ 1 }→ s(plus(activate(N), activate(M))) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U61(z) -{ 1 }→ 0' :|: z = 0
U71(z, z', z'') -{ 1 }→ U72(isNat(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U72(z, z', z'') -{ 1 }→ plus(x(activate(N), activate(M)), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ x(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ s(activate(X)) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ plus(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ 0' :|: z = 0
isNat(z) -{ 1 }→ U31(isNat(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNat(z) -{ 1 }→ U21(isNat(activate(V1))) :|: z = 1 + V1, V1 >= 0
isNat(z) -{ 1 }→ U11(isNat(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNat(z) -{ 1 }→ 0 :|: z = 0
plus(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
x(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
| eq(start(V, V3, V4),0,[fun(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun1(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun2(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun3(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun4(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun5(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun6(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun7(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun8(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun10(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun11(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[isNat(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun9(Out)],[]). eq(start(V, V3, V4),0,[plus(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[s(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[x(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[activate(V, Out)],[V >= 0]). eq(fun(V, V3, Out),1,[activate(V21, Ret00),isNat(Ret00, Ret0),fun1(Ret0, Ret)],[Out = Ret,V3 = V21,V21 >= 0,V = 0]). eq(fun1(V, Out),1,[],[Out = 0,V = 0]). eq(fun2(V, Out),1,[],[Out = 0,V = 0]). eq(fun3(V, V3, Out),1,[activate(V22, Ret001),isNat(Ret001, Ret01),fun4(Ret01, Ret1)],[Out = Ret1,V3 = V22,V22 >= 0,V = 0]). eq(fun4(V, Out),1,[],[Out = 0,V = 0]). eq(fun5(V, V3, Out),1,[activate(N1, Ret2)],[Out = Ret2,V3 = N1,V = 0,N1 >= 0]). eq(fun6(V, V3, V4, Out),1,[activate(N2, Ret002),isNat(Ret002, Ret02),activate(M1, Ret11),activate(N2, Ret21),fun7(Ret02, Ret11, Ret21, Ret3)],[Out = Ret3,V3 = M1,V = 0,V4 = N2,M1 >= 0,N2 >= 0]). eq(fun7(V, V3, V4, Out),1,[activate(N3, Ret003),activate(M2, Ret011),plus(Ret003, Ret011, Ret03),s(Ret03, Ret4)],[Out = Ret4,V3 = M2,V = 0,V4 = N3,M2 >= 0,N3 >= 0]). eq(fun8(V, Out),1,[fun9(Ret5)],[Out = Ret5,V = 0]). eq(fun10(V, V3, V4, Out),1,[activate(N4, Ret004),isNat(Ret004, Ret04),activate(M3, Ret12),activate(N4, Ret22),fun11(Ret04, Ret12, Ret22, Ret6)],[Out = Ret6,V3 = M3,V = 0,V4 = N4,M3 >= 0,N4 >= 0]). eq(fun11(V, V3, V4, Out),1,[activate(N5, Ret005),activate(M4, Ret012),x(Ret005, Ret012, Ret05),activate(N5, Ret13),plus(Ret05, Ret13, Ret7)],[Out = Ret7,V3 = M4,V = 0,V4 = N5,M4 >= 0,N5 >= 0]). eq(isNat(V, Out),1,[],[Out = 0,V = 0]). eq(isNat(V, Out),1,[activate(V11, Ret006),isNat(Ret006, Ret06),activate(V23, Ret14),fun(Ret06, Ret14, Ret8)],[Out = Ret8,V11 >= 0,V23 >= 0,V = 1 + V11 + V23]). eq(isNat(V, Out),1,[activate(V12, Ret007),isNat(Ret007, Ret07),fun2(Ret07, Ret9)],[Out = Ret9,V = 1 + V12,V12 >= 0]). eq(isNat(V, Out),1,[activate(V13, Ret008),isNat(Ret008, Ret08),activate(V24, Ret15),fun3(Ret08, Ret15, Ret10)],[Out = Ret10,V13 >= 0,V24 >= 0,V = 1 + V13 + V24]). eq(fun9(Out),1,[],[Out = 0]). eq(plus(V, V3, Out),1,[],[Out = 1 + X11 + X21,X11 >= 0,X21 >= 0,V = X11,V3 = X21]). eq(s(V, Out),1,[],[Out = 1 + X3,X3 >= 0,V = X3]). eq(x(V, V3, Out),1,[],[Out = 1 + X12 + X22,X12 >= 0,X22 >= 0,V = X12,V3 = X22]). eq(activate(V, Out),1,[fun9(Ret16)],[Out = Ret16,V = 0]). eq(activate(V, Out),1,[activate(X13, Ret09),activate(X23, Ret17),plus(Ret09, Ret17, Ret18)],[Out = Ret18,X13 >= 0,X23 >= 0,V = 1 + X13 + X23]). eq(activate(V, Out),1,[activate(X4, Ret010),s(Ret010, Ret19)],[Out = Ret19,V = 1 + X4,X4 >= 0]). eq(activate(V, Out),1,[activate(X14, Ret013),activate(X24, Ret110),x(Ret013, Ret110, Ret20)],[Out = Ret20,X14 >= 0,X24 >= 0,V = 1 + X14 + X24]). eq(activate(V, Out),1,[],[Out = X5,X5 >= 0,V = X5]). input_output_vars(fun(V,V3,Out),[V,V3],[Out]). input_output_vars(fun1(V,Out),[V],[Out]). input_output_vars(fun2(V,Out),[V],[Out]). input_output_vars(fun3(V,V3,Out),[V,V3],[Out]). input_output_vars(fun4(V,Out),[V],[Out]). input_output_vars(fun5(V,V3,Out),[V,V3],[Out]). input_output_vars(fun6(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun7(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun8(V,Out),[V],[Out]). input_output_vars(fun10(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun11(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(isNat(V,Out),[V],[Out]). input_output_vars(fun9(Out),[],[Out]). input_output_vars(plus(V,V3,Out),[V,V3],[Out]). input_output_vars(s(V,Out),[V],[Out]). input_output_vars(x(V,V3,Out),[V,V3],[Out]). input_output_vars(activate(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun9/1]
1. non_recursive : [plus/3]
2. non_recursive : [s/2]
3. non_recursive : [x/3]
4. recursive [non_tail,multiple] : [activate/2]
5. non_recursive : [fun1/2]
6. non_recursive : [fun2/2]
7. non_recursive : [fun4/2]
8. recursive [non_tail,multiple] : [fun/3,fun3/3,isNat/2]
9. non_recursive : [fun11/4]
10. non_recursive : [fun10/4]
11. non_recursive : [fun5/3]
12. non_recursive : [fun7/4]
13. non_recursive : [fun6/4]
14. non_recursive : [fun8/2]
15. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is completely evaluated into other SCCs
1. SCC is completely evaluated into other SCCs
2. SCC is completely evaluated into other SCCs
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into activate/2
5. SCC is completely evaluated into other SCCs
6. SCC is completely evaluated into other SCCs
7. SCC is completely evaluated into other SCCs
8. SCC is partially evaluated into isNat/2
9. SCC is partially evaluated into fun11/4
10. SCC is partially evaluated into fun10/4
11. SCC is completely evaluated into other SCCs
12. SCC is partially evaluated into fun7/4
13. SCC is partially evaluated into fun6/4
14. SCC is completely evaluated into other SCCs
15. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations activate/2
* CE 12 is refined into CE [23]
* CE 15 is refined into CE [24]
* CE 14 is refined into CE [25]
* CE 13 is refined into CE [26]
### Cost equations --> "Loop" of activate/2
* CEs [26] --> Loop 12
* CEs [25] --> Loop 13
* CEs [23,24] --> Loop 14
### Ranking functions of CR activate(V,Out)
* RF of phase [12,13]: [V]
#### Partial ranking functions of CR activate(V,Out)
* Partial RF of phase [12,13]:
- RF of loop [12:1,12:2,13:1]:
V
### Specialization of cost equations isNat/2
* CE 18 is refined into CE [27]
* CE 17 is refined into CE [28]
* CE 16 is refined into CE [29]
### Cost equations --> "Loop" of isNat/2
* CEs [29] --> Loop 15
* CEs [28] --> Loop 16
* CEs [27] --> Loop 17
### Ranking functions of CR isNat(V,Out)
* RF of phase [15,17]: [V]
#### Partial ranking functions of CR isNat(V,Out)
* Partial RF of phase [15,17]:
- RF of loop [15:1,15:2,17:1]:
V
### Specialization of cost equations fun11/4
* CE 22 is refined into CE [30]
### Cost equations --> "Loop" of fun11/4
* CEs [30] --> Loop 18
### Ranking functions of CR fun11(V,V3,V4,Out)
#### Partial ranking functions of CR fun11(V,V3,V4,Out)
### Specialization of cost equations fun10/4
* CE 21 is refined into CE [31,32]
### Cost equations --> "Loop" of fun10/4
* CEs [32] --> Loop 19
* CEs [31] --> Loop 20
### Ranking functions of CR fun10(V,V3,V4,Out)
#### Partial ranking functions of CR fun10(V,V3,V4,Out)
### Specialization of cost equations fun7/4
* CE 20 is refined into CE [33]
### Cost equations --> "Loop" of fun7/4
* CEs [33] --> Loop 21
### Ranking functions of CR fun7(V,V3,V4,Out)
#### Partial ranking functions of CR fun7(V,V3,V4,Out)
### Specialization of cost equations fun6/4
* CE 19 is refined into CE [34,35]
### Cost equations --> "Loop" of fun6/4
* CEs [35] --> Loop 22
* CEs [34] --> Loop 23
### Ranking functions of CR fun6(V,V3,V4,Out)
#### Partial ranking functions of CR fun6(V,V3,V4,Out)
### Specialization of cost equations start/3
* CE 2 is refined into CE [36,37]
* CE 3 is refined into CE [38]
* CE 4 is refined into CE [39]
* CE 5 is refined into CE [40,41]
* CE 6 is refined into CE [42]
* CE 7 is refined into CE [43]
* CE 8 is refined into CE [44,45]
* CE 9 is refined into CE [46]
* CE 10 is refined into CE [47,48]
* CE 11 is refined into CE [49]
### Cost equations --> "Loop" of start/3
* CEs [36,37,38,39,40,41,42,43,44,45,46,47,48,49] --> Loop 24
### Ranking functions of CR start(V,V3,V4)
#### Partial ranking functions of CR start(V,V3,V4)
Computing Bounds
=====================================
#### Cost of chains of activate(V,Out):
* Chain [14]: 2
with precondition: [V=Out,V>=0]
* Chain [multiple([12,13],[[14]])]: 4*it(12)+2*it([14])+0
Such that:it([14]) =< V+1
aux(1) =< V
it(12) =< aux(1)
with precondition: [V=Out,V>=1]
#### Cost of chains of isNat(V,Out):
* Chain [16]: 1
with precondition: [V=0,Out=0]
* Chain [multiple([15,17],[[16]])]: 13*it(15)+1*it([16])+2*s(25)+4*s(26)+10*s(27)+8*s(28)+0
Such that:it([16]) =< V+1
aux(10) =< V
it(15) =< aux(10)
aux(6) =< aux(10)+1
aux(7) =< aux(10)
s(29) =< it(15)*aux(10)
s(31) =< it(15)*aux(6)
s(30) =< it(15)*aux(7)
s(25) =< it(15)*aux(6)
s(27) =< s(31)
s(28) =< s(30)
s(26) =< s(29)
with precondition: [Out=0,V>=1]
#### Cost of chains of fun11(V,V3,V4,Out):
* Chain [18]: 4*s(35)+8*s(36)+2*s(38)+4*s(39)+9
Such that:s(37) =< V3
s(38) =< V3+1
aux(11) =< V4
aux(12) =< V4+1
s(35) =< aux(12)
s(36) =< aux(11)
s(39) =< s(37)
with precondition: [V=0,V3+2*V4+2=Out,V3>=0,V4>=0]
#### Cost of chains of fun10(V,V3,V4,Out):
* Chain [20]: 8*s(44)+4*s(47)+8*s(48)+17
Such that:aux(14) =< 1
aux(15) =< V3
aux(16) =< V3+1
s(44) =< aux(14)
s(47) =< aux(16)
s(48) =< aux(15)
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [19]: 9*s(60)+29*s(61)+2*s(70)+10*s(71)+8*s(72)+4*s(73)+4*s(75)+8*s(76)+16
Such that:aux(17) =< V3
aux(18) =< V3+1
aux(19) =< V4
aux(20) =< V4+1
s(75) =< aux(18)
s(60) =< aux(20)
s(61) =< aux(19)
s(76) =< aux(17)
s(65) =< aux(19)+1
s(66) =< aux(19)
s(67) =< s(61)*aux(19)
s(68) =< s(61)*s(65)
s(69) =< s(61)*s(66)
s(70) =< s(61)*s(65)
s(71) =< s(68)
s(72) =< s(69)
s(73) =< s(67)
with precondition: [V=0,V3+2*V4+2=Out,V3>=0,V4>=1]
#### Cost of chains of fun7(V,V3,V4,Out):
* Chain [21]: 2*s(88)+4*s(89)+2*s(91)+4*s(92)+7
Such that:s(90) =< V3
s(91) =< V3+1
s(87) =< V4
s(88) =< V4+1
s(92) =< s(90)
s(89) =< s(87)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=0]
#### Cost of chains of fun6(V,V3,V4,Out):
* Chain [23]: 6*s(94)+4*s(97)+8*s(98)+15
Such that:aux(22) =< 1
aux(23) =< V3
aux(24) =< V3+1
s(94) =< aux(22)
s(97) =< aux(24)
s(98) =< aux(23)
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [22]: 7*s(109)+25*s(110)+2*s(119)+10*s(120)+8*s(121)+4*s(122)+4*s(124)+8*s(125)+14
Such that:aux(25) =< V3
aux(26) =< V3+1
aux(27) =< V4
aux(28) =< V4+1
s(124) =< aux(26)
s(109) =< aux(28)
s(125) =< aux(25)
s(110) =< aux(27)
s(114) =< aux(27)+1
s(115) =< aux(27)
s(116) =< s(110)*aux(27)
s(117) =< s(110)*s(114)
s(118) =< s(110)*s(115)
s(119) =< s(110)*s(114)
s(120) =< s(117)
s(121) =< s(118)
s(122) =< s(116)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=1]
#### Cost of chains of start(V,V3,V4):
* Chain [24]: 16*s(136)+25*s(139)+61*s(140)+2*s(149)+10*s(150)+8*s(151)+4*s(152)+22*s(167)+66*s(169)+4*s(175)+20*s(176)+16*s(177)+8*s(178)+3*s(215)+17*s(217)+2*s(223)+10*s(224)+8*s(225)+4*s(226)+17
Such that:aux(31) =< 1
aux(32) =< V
aux(33) =< V+1
aux(34) =< V3
aux(35) =< V3+1
aux(36) =< V4
aux(37) =< V4+1
s(136) =< aux(31)
s(215) =< aux(33)
s(139) =< aux(35)
s(167) =< aux(37)
s(140) =< aux(34)
s(217) =< aux(32)
s(218) =< aux(32)+1
s(219) =< aux(32)
s(220) =< s(217)*aux(32)
s(221) =< s(217)*s(218)
s(222) =< s(217)*s(219)
s(223) =< s(217)*s(218)
s(224) =< s(221)
s(225) =< s(222)
s(226) =< s(220)
s(144) =< aux(34)+1
s(145) =< aux(34)
s(146) =< s(140)*aux(34)
s(147) =< s(140)*s(144)
s(148) =< s(140)*s(145)
s(149) =< s(140)*s(144)
s(150) =< s(147)
s(151) =< s(148)
s(152) =< s(146)
s(169) =< aux(36)
s(170) =< aux(36)+1
s(171) =< aux(36)
s(172) =< s(169)*aux(36)
s(173) =< s(169)*s(170)
s(174) =< s(169)*s(171)
s(175) =< s(169)*s(170)
s(176) =< s(173)
s(177) =< s(174)
s(178) =< s(172)
with precondition: []
Closed-form bounds of start(V,V3,V4):
-------------------------------------
* Chain [24] with precondition: []
- Upper bound: nat(V)*29+33+nat(V)*24*nat(V)+nat(V3)*73+nat(V3)*24*nat(V3)+nat(V4)*90+nat(V4)*48*nat(V4)+nat(V+1)*3+nat(V3+1)*25+nat(V4+1)*22
- Complexity: n^2
### Maximum cost of start(V,V3,V4): nat(V)*29+33+nat(V)*24*nat(V)+nat(V3)*73+nat(V3)*24*nat(V3)+nat(V4)*90+nat(V4)*48*nat(V4)+nat(V+1)*3+nat(V3+1)*25+nat(V4+1)*22
Asymptotic class: n^2
* Total analysis performed in 448 ms.